Nuprl Lemma : init-p-realizable
11,40
postcript
pdf
T
:Type,
v
:
T
,
x
,
i
:Id. es-real{i:l}(
es
.init-p(
es
;
i
;
T
;
x
;
v
))
latex
Definitions
x
:
A
.
B
(
x
)
,
event_system{i:l}
,
t
T
,
init-p(
es
;
i
;
T
;
x
;
v
)
,
Type
,
prop{i:l}
,
x
.
t
(
x
)
,
R-realizes{i:l}(
R
;
es
.
P
(
es
))
,
rationals
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
es-real{i:l}(
es
.
P
(
es
))
,
Id
,
inl
x
,
Rinit(
loc
;
T
;
x
;
v
)
Lemmas
Id
wf
,
Rinit
wf
,
rationals
wf
,
R-realizes
wf
,
init-p
wf
,
event
system
wf
,
R-init-rule
origin
T:Type, v:T, x,i:Id. es-real{i:l}(es.init-p(es; i; T; x; v)) T:Type, v:T, x,i:Id. es-real{i:l}(es.init-p(es; i; T; x; v)) 
T
x. t(x)
B(x)
x:A. B(x)